(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 11))
(declare-fun v1 () (_ BitVec 3))
(declare-fun a2 () (Array  (_ BitVec 8)  (_ BitVec 3)))
(assert (let ((e3(_ bv1 3)))
(let ((e4(_ bv1 3)))
(let ((e5 (bvurem e3 v1)))
(let ((e6 (bvsrem ((_ sign_extend 8) e5) v0)))
(let ((e7 (ite (bvugt e3 v1) (_ bv1 1) (_ bv0 1))))
(let ((e8 (bvnot e7)))
(let ((e9 ((_ rotate_right 0) e7)))
(let ((e10 (bvudiv e7 e7)))
(let ((e11 (bvor e5 e4)))
(let ((e12 (store a2 ((_ sign_extend 5) e3) e11)))
(let ((e13 (select e12 ((_ extract 7 0) v0))))
(let ((e14 (store a2 ((_ zero_extend 7) e8) ((_ extract 9 7) v0))))
(let ((e15 (ite (bvsge e6 ((_ sign_extend 8) e5)) (_ bv1 1) (_ bv0 1))))
(let ((e16 (bvurem e11 e11)))
(let ((e17 (ite (= v0 ((_ sign_extend 8) e13)) (_ bv1 1) (_ bv0 1))))
(let ((e18 (bvnand ((_ sign_extend 10) e10) e6)))
(let ((e19 (bvcomp ((_ zero_extend 2) e9) v1)))
(let ((e20 (bvshl e3 ((_ sign_extend 2) e15))))
(let ((e21 (bvxor e5 ((_ sign_extend 2) e19))))
(let ((e22 (bvshl e4 v1)))
(let ((e23 (ite (bvsge e7 e7) (_ bv1 1) (_ bv0 1))))
(let ((e24 (bvor e8 e19)))
(let ((e25 (bvsgt e3 ((_ zero_extend 2) e8))))
(let ((e26 (bvule e21 e22)))
(let ((e27 (bvsge ((_ zero_extend 2) e7) e5)))
(let ((e28 (= ((_ zero_extend 10) e23) e6)))
(let ((e29 (bvule e11 ((_ zero_extend 2) e19))))
(let ((e30 (bvuge e18 ((_ sign_extend 10) e9))))
(let ((e31 (distinct e23 e15)))
(let ((e32 (bvslt ((_ zero_extend 2) e17) e4)))
(let ((e33 (bvsle e6 ((_ sign_extend 10) e9))))
(let ((e34 (bvugt e4 e22)))
(let ((e35 (distinct ((_ sign_extend 10) e24) e18)))
(let ((e36 (distinct e20 e4)))
(let ((e37 (bvsgt v1 ((_ zero_extend 2) e10))))
(let ((e38 (bvuge e18 ((_ zero_extend 8) e3))))
(let ((e39 (bvuge e3 ((_ zero_extend 2) e9))))
(let ((e40 (bvult ((_ sign_extend 8) e3) v0)))
(let ((e41 (bvsge ((_ sign_extend 2) e17) e13)))
(let ((e42 (bvsgt e8 e24)))
(let ((e43 (distinct e22 e21)))
(let ((e44 (bvugt e13 ((_ sign_extend 2) e9))))
(let ((e45 (bvsge e10 e17)))
(let ((e46 (distinct e4 e13)))
(let ((e47 (bvule e18 ((_ zero_extend 8) e13))))
(let ((e48 (bvuge ((_ sign_extend 10) e17) e18)))
(let ((e49 (bvslt e11 e22)))
(let ((e50 (bvult e5 ((_ sign_extend 2) e19))))
(let ((e51 (bvslt e9 e9)))
(let ((e52 (bvslt e18 ((_ zero_extend 10) e17))))
(let ((e53 (bvslt e3 e5)))
(let ((e54 (= e15 e23)))
(let ((e55 (= e10 e10)))
(let ((e56 (bvuge v1 ((_ sign_extend 2) e15))))
(let ((e57 (bvsle v0 ((_ zero_extend 10) e17))))
(let ((e58 (bvuge e4 ((_ zero_extend 2) e9))))
(let ((e59 (bvsge e5 v1)))
(let ((e60 (distinct e20 e22)))
(let ((e61 (bvuge e11 e13)))
(let ((e62 (bvslt ((_ sign_extend 2) e8) e21)))
(let ((e63 (bvugt ((_ sign_extend 2) e15) e13)))
(let ((e64 (= e20 e13)))
(let ((e65 (bvuge v1 e13)))
(let ((e66 (= e4 ((_ zero_extend 2) e9))))
(let ((e67 (bvsle e9 e9)))
(let ((e68 (bvugt e3 e20)))
(let ((e69 (bvslt e5 ((_ zero_extend 2) e8))))
(let ((e70 (bvult e5 e3)))
(let ((e71 (= ((_ zero_extend 8) e22) v0)))
(let ((e72 (bvsge e21 e5)))
(let ((e73 (bvuge e7 e23)))
(let ((e74 (bvule v1 e22)))
(let ((e75 (bvugt ((_ zero_extend 2) e15) e21)))
(let ((e76 (bvslt e20 e5)))
(let ((e77 (bvult e22 e13)))
(let ((e78 (bvsge e18 ((_ sign_extend 10) e15))))
(let ((e79 (distinct ((_ sign_extend 8) e20) e6)))
(let ((e80 (distinct e16 ((_ zero_extend 2) e7))))
(let ((e81 (not e30)))
(let ((e82 (or e38 e67)))
(let ((e83 (ite e52 e71 e26)))
(let ((e84 (= e29 e58)))
(let ((e85 (ite e83 e79 e69)))
(let ((e86 (xor e55 e55)))
(let ((e87 (= e53 e73)))
(let ((e88 (and e84 e56)))
(let ((e89 (ite e66 e81 e85)))
(let ((e90 (or e32 e35)))
(let ((e91 (= e57 e72)))
(let ((e92 (or e90 e47)))
(let ((e93 (xor e60 e78)))
(let ((e94 (or e49 e54)))
(let ((e95 (or e36 e93)))
(let ((e96 (xor e77 e45)))
(let ((e97 (ite e87 e37 e92)))
(let ((e98 (ite e68 e27 e89)))
(let ((e99 (=> e88 e64)))
(let ((e100 (and e31 e41)))
(let ((e101 (not e82)))
(let ((e102 (and e99 e96)))
(let ((e103 (= e101 e97)))
(let ((e104 (or e34 e46)))
(let ((e105 (or e25 e102)))
(let ((e106 (ite e105 e98 e42)))
(let ((e107 (not e33)))
(let ((e108 (= e63 e74)))
(let ((e109 (or e50 e61)))
(let ((e110 (ite e76 e103 e108)))
(let ((e111 (and e107 e107)))
(let ((e112 (not e70)))
(let ((e113 (or e59 e44)))
(let ((e114 (=> e91 e106)))
(let ((e115 (and e111 e39)))
(let ((e116 (xor e65 e95)))
(let ((e117 (ite e104 e115 e113)))
(let ((e118 (=> e40 e114)))
(let ((e119 (or e109 e62)))
(let ((e120 (= e28 e117)))
(let ((e121 (xor e48 e116)))
(let ((e122 (=> e121 e118)))
(let ((e123 (and e86 e80)))
(let ((e124 (= e122 e112)))
(let ((e125 (not e120)))
(let ((e126 (xor e123 e51)))
(let ((e127 (xor e110 e119)))
(let ((e128 (and e124 e126)))
(let ((e129 (= e100 e43)))
(let ((e130 (ite e128 e128 e94)))
(let ((e131 (and e130 e127)))
(let ((e132 (or e125 e131)))
(let ((e133 (ite e75 e132 e129)))
(let ((e134 (and e133 (not (= v1 (_ bv0 3))))))
(let ((e135 (and e134 (not (= v0 (_ bv0 11))))))
(let ((e136 (and e135 (not (= v0 (bvnot (_ bv0 11)))))))
(let ((e137 (and e136 (not (= e11 (_ bv0 3))))))
(let ((e138 (and e137 (not (= e7 (_ bv0 1))))))
e138
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
